ErasedMacro1.agda:15,5-6
Identifier A is declared erased, so it cannot be used here
when inferring the type of A
